$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $a$:$T$, $L$:($T$ List).
\\[0ex]no\_repeats($T$; $L$) $\Rightarrow$ no\_repeats($T$; insert(${\it eq}$; $a$; $L$))